\section{M\'odulo Cola De Prioridad Modificable}

    \subsection{TAD}
    
    \begin{tad}{\tadNombre{Cola de Prioridad Modificable($\alpha$)}}
    
    \tadIgualdadObservacional{c}{c'}{colaPrior($\alpha$)}{limite($c$) $\igobs$ limite($c'$) $\land$ \\ 
                                                     vacia?($c$) $\igobs$ vacia?($c'$) $\land$ \\ 
                                                     ($\neg$ vacia?($c$) $\implies$ (proximo($c$) $\igobs$ proximo($c'$) $\land$ \\
                                            \phantom{($\neg$vacía?($c$) $\implies$ (}desencolar($c$) $\igobs$ desencolar($c'$))}
                                                        
    
    \tadParametrosFormales{
        \tadEncabezadoInline{generos}{$\alpha$}\\
        \tadEncabezadoInline{operaciones}{
            \tadOperacionInline{\argumento $<$ \argumento}{$\alpha$, $\alpha$}{bool} \hfill Relacion de orden total estricto\footnotemark
        }
    }

    \footnotetext{\noindent Una relacion es un orden total estricto cuando se cumple:
    \begin{description}
     \item[Antirreflexividad:] $\neg$ $a < a$ para todo $a: \alpha$
     \item[Antisimetria:] $(a < b \implies \neg\ b < a)$ para todo $a, b: \alpha$
     \item[Transitividad:] $((a < b \land b < c) \implies a < c)$ para todo $a, b, c: \alpha$
     \item[Totalidad:] $(a < b \lor b < a)$ para todo $a, b: \alpha$
    \end{description}
    }

    \tadGeneros{colaPrior($\alpha$)}
    \tadExporta{colaPrior($\alpha$), generadores, observadores}
    \tadUsa{\tadNombre{Bool}}

    \tadAlinearFunciones{desencolar}{$\alpha$,colaPrior($\alpha$),nat/n}

    \tadObservadores
    \tadOperacion{vacia?}{colaPrior($\alpha$)}{bool}{}
    \tadOperacion{limite}{colaPrior($\alpha$)}{nat}{}
    \tadOperacion{proximo}{colaPrior($\alpha$)/c}{$\alpha$}{($\neg$ vacia?($c$))}
    \tadOperacion{desencolar}{colaPrior($\alpha$)/c}{colaPrior($\alpha$)}{($\neg$ vacia?($c$))}

    \tadGeneradores
    \tadOperacion{vacia}{nat/n}{colaPrior($\alpha$)}{$n > 0$}
    \tadOperacion{encolar}{$\alpha$,colaPrior($\alpha$)/c}{colaPrior($\alpha$)}{tamanio(c) $<$ limite(c)}

    \tadOtrasOperaciones
    \tadAlinearFunciones{tamanio}{colaPrior($\alpha$)}
    \tadOperacion{tamanio}{colaPrior($\alpha$)}{nat}{}

    \tadAxiomas[\paratodo{colaPrior($\alpha$)}{c}, \paratodo{$\alpha$}{e}]
    \tadAlinearAxiomas{desencolar(encolar($e$, $c$))}{}

    \tadAxioma{vacia?(vacia)}{true}
    \tadAxioma{vacia?(encolar($e$, $c$))}{false}

    \tadAxioma{proximo(encolar($e$, $c$))}{\IF vacia?($c$) $\lor$\ proximo($c$) $< e$ THEN $e$ ELSE proximo($c$) FI}

    \tadAxioma{desencolar(encolar($e$, $c$))}{\IF vacia?($c$) $\lor$\ proximo($c$) $< e$ THEN $c$ ELSE encolar($e$, desencolar($c$)) FI}
    
    \tadAxioma{tamanio($c$)}{\IF vacia?($c$) THEN 0 ELSE 1 + tamanio(desencolar($c$)) FI}

    \end{tad}

	\subsection{Interfaz}

        \begin{interfaces}
            {Cola De Prioridad}
            {$\alpha$}
            {$\alpha$}
            {Vector}
            {colaPrior($\alpha$)}
            {colaPrior($\alpha$)}

		\subsubsection*{Observadores}
	        \interfaz{ColaVacia?}{\parametro{in}{c}{colaPrior($\alpha$)}}{bool}
			        {true} 
			        {res $\igobs$ ColaVacia?(c)}
			        {\complejidad{$Theta$}{1}}{}
			        {}
			        {Devuelve true si la cola $c$ esta vac\'ia.}

	        \interfaz{Proximo}{\parametro{in}{c}{colaPrior($\alpha$)}}{$\alpha$}
			        {$\lnot$ ColaVacia?(c)} 
			        {res $\igobs$ Proximo(c)}
			        {\complejidad{$\Theta$}{1}}{}
			        {El resultado tiene aliasing con el elemento de la cola.}
			        {Devuelve el pr\'oximo valor de la cola}

		\interfaz{Desencolar}{\parametro{in/out}{c}{colaPrior($\alpha$)}}{}
			        {$c_0$ $\igobs$ $c$ $\land$ $\lnot$ ColaVacia?(c)} 
			        {c $\igobs$ desencolar($c_0$)}
			        {\complejidad{O}{log(n)}}{}
			        {}
			        {Desencola el pr\'oximo elemento de la cola.}

		\subsubsection*{Generadores}
		\interfaz{ColaVacia}{\parametro{in}{nat}{cant}}{colaPrior($\alpha$)}
			        {true} 
			        {res $\igobs$ vacia()}
			        {\complejidad{O}{cant}}{}
			        {}
			        {Crea una cola de prioridad que puede contener como m\'aximo $cant$ elementos.}

		\interfaz{Encolar}{\parametro{in/out}{c}{colaPrior($\alpha$)}, \parametro{in}{a}{$\alpha$}}{}
			        {$c_0 $\igobs$ c \land tamanio(c) < limite(c)$} 
			        {$c \igobs$ encolar($c_0, a$)}
			        {\complejidad{O}{log(n) + copy($\alpha$)}}{}
			        {}
			        {Encola el elemento $a$.}

		\interfaz{Limite}{\parametro{in}{c}{colaPrior($\alpha$)}}{nat}
			        {true} 
			        {$res \igobs$ limite(c)}
			        {\complejidad{$\Theta$}{1}}{}
			        {}
			        {Devuelve el tama\~no m\'aximo de elementos que puede contener la cola.}

		\subsubsection*{Otras Operaciones}	        
		\interfaz{Tamanio}{\parametro{in}{c}{colaPrior($\alpha$)}}{nat}
			        {true} 
			        {$res \igobs$ tamanio($c$)}
			        {\complejidad{$\Theta$}{1}}{}
			        {}
			        {Retorna la cantidad de elementos encolados actualmente.}

		\interfaz{Actualizar}{\parametro{in/out}{c}{colaPrior($\alpha$)}, \parametro{in}{actual}{$\alpha$}, \parametro{in}{nuevo}{$\alpha$}}{}
			        {$c_0$ $\igobs$ $c$ $\land$ $\lnot$ ColaVacia?($c$)} 
			        {$c \igobs$}
			        {\complejidad{O}{log(n)}}{Siendo n la cantidad de elementos en la cola.}
			        {}
			        {Se actualiza el elemento en la cola. En el peor caso, el elemento a actualizar está en la primera posici\'on, 
				 por lo que obtenerlo cuesta O(log(n)), borrarlo cuesta log(n) y encolarlo de nuevo cuesta log(n)}
        \end{interfaces}

  \subsection{Representaci\'on}
	
	\representacion{colaPrior($\alpha$)}{se representa con}{estrCola},
      donde \representacion{estrCola}{es}{}
    \begin{definicionTupla}
	\elementoTupla{cantidad}{nat},\\
	\elementoTupla{limite}{nat},\\
	\elementoTupla{nodos}{arreglo\_dimensionable(puntero($\alpha$))}\\
    \end{definicionTupla}
	
  \subsection{Algoritmos}
	
	\begin{codebox}
	\encabezadoFuncion{iColaVacia?}{\parametro{in}{c}{estrCola}}{bool}\\
	\li $res \gets$ \attrib{c}{cantidad} $\isequal$ 0
	\end{codebox}

    Esta funcion es claramente \complejidad{$\Theta$}{1} pues solo asigna un bool y compara 2 naturales.
    
    \begin{codebox}
    \encabezadoFuncion{Proximo}{\parametro{in}{c}{colaPrior($\alpha$)}}{$\alpha$}\\
	\li $res \gets *(c.nodos[0])$
	\end{codebox}

    Esta funcion es claramente \complejidad{$\Theta$}{1} pues solo indexa un arreglo y apuntar un puntero.
    
    
    \begin{codebox}
    \encabezadoFuncion{Proximo}{\parametro{in}{c}{colaPrior($\alpha$)}}{$\alpha$}\\
	\li $res \gets *(c.nodos[0])$
	\end{codebox}

    Esta funcion es claramente \complejidad{$\Theta$}{1} pues solo indexa un arreglo y apuntar un puntero.
    
    \begin{codebox}
    \encabezadoFuncion{Desencolar}{\parametro{in/out}{c}{colaPrior($\alpha$)}}{}\\
    \li implementar
	\end{codebox}

    Esta funcion es claramente \complejidad{$\Theta$}{1} pues solo retorna un nat
    
    \begin{codebox}
    \encabezadoFuncion{ColaVacia}{\parametro{in}{nat}{cant}}{colaPrior($\alpha$)}\\
	\li $res \gets$ \tupla{$cant, \proc{CrearArreglo}(cant$)}
	\li $i \gets 0$
	\li \While $i < cant$
	\li \Do
		$res.nodos[i] \gets NULL$
	\li 	$i \gets i + 1$
	    \End
    \end{codebox}

    Esta funcion es \complejidad{O}{$cant$}, pues la primera l\'inea es \complejidad{O}{1}, y el ciclo esta acotado por cant, y dentro de este solo se hace una asignacion de un puntero.
    
    \begin{codebox}
    \encabezadoFuncion{Encolar}{\parametro{in/out}{c}{colaPrior($\alpha$)}, \parametro{in}{a}{$\alpha$}}{}\\
    \li implementar
	\end{codebox}
    
    \begin{codebox}
    \encabezadoFuncion{Tamanio}{\parametro{in}{c}{colaPrior($\alpha$)}}{nat}\\
	\li $res \gets \attrib{c}{cantidad}$
	\end{codebox}

    Esta funcion es claramente \complejidad{$\Theta$}{1} pues solo retorna un nat

    \begin{codebox}
    \encabezadoFuncion{Actualizar}{\parametro{in/out}{c}{colaPrior($\alpha$)}, \parametro{in}{actual}{$\alpha$}, \parametro{in}{nuevo}{$\alpha$}}{}\\
    \li implementar
    \end{codebox}


  \subsection{Servicios Utilizados}
